;;;
;;; Solution for A3 question #1
;;;
;;; Philip W. L. Fong
;;;

;;
;; Skolemize
;;

(defun skolemize (wff)
  "Skolemize formula WFF."
  (skolemize-aux wff nil))

(defun skolemize-aux (wff var-list)
  "Skolemize formula WFF, assuming that the variables in the list
VAR-LIST are implicitly quantified universally."
  (cond
   ((universal-p wff)
    (make-universal (universal-var wff)
		    (skolemize-aux (universal-wff wff) 
				   (cons (universal-var wff) var-list))))
   ((existential-p wff)
    (skolemize-aux (wff-substitute (existential-wff wff)
				   (existential-var wff)
				   (generate-skolem-function var-list))
		   var-list))
   (t wff)))


;;
;; Preprocess
;;

(defun preprocess (wff &optional (debug t))
  "Preprocess formula WFF.  Set the optional argument DEBUG to NIL for
silent mode."
  (if debug
    (format t "Preprocess Formula:~%~S~%" wff))
  (setf wff (eliminate-implications wff))
  (if debug
    (format t "Eliminate Implications:~%~S~%" wff))
  (setf wff (move-negations-inwards wff))
  (if debug
    (format t "Move Negations Inwards:~%~S~%" wff))
  (setf wff (standardize-variables wff))
  (if debug
    (format t "Standardize Variables:~%~S~%" wff))
  (setf wff (move-quantifiers-left wff))
  (if debug
    (format t "Move Quantifiers Left:~%~S~%" wff))
  (setf wff (skolemize wff))
  (if debug
    (format t "Skolemize:~%~S~%" wff))
  (setf wff (distribute-disj-over-conj wff))
  (if debug
    (format t "Distribute Disjunction Over Conjunction:~%~S~%" wff))
  (setf wff (clausal-form wff))
  (if debug
    (format t "Convert to Clausal Form:~%~S~%" wff))
  wff)


